perm filename A09.TEX[257,RWF] blob sn#847486 filedate 1987-10-26 generic text, type C, neo UTF8
COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnification\magstephalf
C00008 ENDMK
C⊗;
\magnification\magstephalf
\input macro.tex
\def\today{\ifcase\month\or
  January\or February\or March\or April\or May\or June\or
  July\or August\or September\or October\or November\or December\fi
  \space\number\day, \number\year}
\baselineskip 14pt
\def\fnc#1{\mathop{\rm #1}\nolimits}
\def\ld{\mathrel{\hbox{$<$\kern-4pt$\cdot$}}}
\def\gd{\mathrel{\hbox{$\cdot$\kern-4pt$>$}}}
\rm
%\font\rmn=amr9
\line{\sevenrm a09.tex[257,phy] \today\hfill}


\def\boxb{\boxbinarya{$\scriptstyle a$}}
\def\boxbb{\boxbinarya{$\scriptstyle b$}}

\noindent{\bf The speedup theorem.} [Fragmentary]

We will define a certain program $p(w,v,x)$ of index~$k$. Applying
the s-m-n theorem to $w$,~$v$, gives a program of one argument,
$p↓{w,v}(x)=\phi↓{s(k,w,v)}(x)$. We will say that program~$i$
is cancellable at $x$ if $\Phi↓i(x)<g↓x\bigl(\max↓{j≤x}\Phi↓{p(i+1,j)}(x)\bigr)$.
Program $p↓{w,v}(x)$ computes an ordered pair
$\langle f↓{w,v}(x),c↓{w,v}(x)\rangle$, where $f↓{w,v}(x)$
is a 0--1 valued cancellation function, and $c↓{w,v}(x)$ is a
finite set of functions known to be cancelled on arguments
$≤x$. The {\it speedup function\/} is $f(0,0)$.

Like other cancellation programs, $p↓{w,v}(x)$ only computes values
of $\phi↓i(x)$ such that $i≤x$; this keeps its task finite,
for each~$x$. It also makes no attempt to cancel $\phi↓i(x)$
if $i<w$ and $x≥v$.  Thus it only tries to cancel $\phi↓i$
at $x$ if $\langle i,x\rangle$ is in the shaded region shown.

\figbox{1.5truein}:

For each program $\phi↓i$, 
there is at most one $x$ such that $p↓{0,0}(x)$
cancels $\phi↓i$ at~$x$. Let $m↓i$ be that $x$ plus~1, if one
exists; if not, let $m↓i=0$. Let $v↓w=\max↓{i<w}m↓i$; then for each~$w$,
$p↓{0,0}(x)$ cancels no program less than $w$ at an $x≥v↓w$, so $p↓{w,v↓w}$
cancels exactly the same programs, and computes exactly the same
function, as~$p↓{0,0}$; in particular $f↓{w,v↓w}=f↓{0,0}$ is the
speedup function. If some program~$\phi↓i$ computes the speedup
function, we see that program $p↓{i+1,v↓{i+1}}$ also computes it,
and because $\phi↓i$ is not cancelled by $p↓{0,0}$,
$$\Phi↓i(x)≥g↓x\bigl(\Phi↓{p↓{i+1,v↓{i+1}}}(x)\bigr)
\quad\hbox{for almost all }x\,,$$
so $p↓{i+1,v↓{i+1}}$ is a $g$-speedup of~$\phi↓i$.

We need to show that $\phi↓{p↓{w,v}}(x)$ is defined for all
$w$, $v$, $x$. Assume defined for the shaded region below, for all~$v$.

%\vfill\eject

When $p↓{w,v}(x)$ is evaluated, a recursion gets $p↓{w,v}(x-1)$,
which by induction hypothesis is defined, and gets $c↓{w,v}(x-1)$
from it by projection. It then, trying to cancel some $\phi↓i$
with $w≤i<x$, evaluates and measures $\phi↓{p↓{i+1,j}}(x)$, which
is also in the shaded region. [RWF: redo paragraph.]

\vfill\eject

%\smallskip
$$\vcenter{\halign{$\rt{#}\quad$&$\lft{#}$\cr
&v=0\quad 1\quad 2\quad 3\quad 4\quad 5\quad 6\quad 7\quad 8\quad 9\quad
10\quad 11\quad 12\quad 13\quad 14\cr
\noalign{\vskip 8pt}
w=0\cr 1\cr 2\cr 3\cr 4\cr 5\cr 6\cr 7\cr 8\cr 9\cr 10\cr}}$$

\smallskip

$C↓{w,v}(x)=$ set of programs cancelled by $p↓{w,v}$ on args $y≤x$,
$=C↓{w,v}(x-1)+\hbox{ any}$ program cancelled at~$x$. $p↓{w,v}(x)$ tries to
cancel $\phi↓i$ at~$x$ if:

\disleft 20pt:(1):$i<x$;
\disleft 20pt:(2):$i\notin C↓{w,v}(x-1)$;
\disleft 20pt:(3):for some $j≤x$, $\Phi↓i(x)<g↓x\bigl(\Phi↓{q↓{i+1,j}}(x)\bigr)\,;$
\disleft 20pt:(4):$x<v$ or $i≥w$.

\bigskip
\parindent0pt
\copyright 1984 Robert W. Floyd
First draft (not published) April 12, 1984.

\bye